With the constant increase in digital circuit complexity, multiple levels of abstraction in circuit representation are typically needed. Register-Transfer Level (RTL) is a technique for describing a circuit at a high level of Boolean functionality and data flow. RTL is one of the preferred abstraction levels for certain kinds of functional designs. Although an RTL design can provide a reference for design implementation, it must be translated into an equivalent switch level design to fabricate the actual integrated circuit.
Gate level and switch level representations are two other forms of circuit representations that are commonly used in simulation of the operation of integrated circuits. A gate level representation can be used to provide a schematic description of circuit components as interconnections of basic blocks having known Boolean functionalities. A switch level representation provides a representation of switches (transistors) and gates that implement the desired functionality for a particular circuit. For an integrated circuit to meet strict operating criteria in terms of speed, power, and surface area, it is generally necessary to create custom designs at the switch level. However, traditional techniques for verifying such designs are generally expensive and can incur errors.
“Formal verification” techniques can be used to prove the accuracy of the design and generally require less effort and computer resources than traditional verification techniques. “Formal equivalence checking” is one of the most widely used formal verification techniques for VLSI design. Most current tools employ formal methods at the RTL and gate level. This paradigm is acceptable for many ASIC designs that rely on logic synthesis. However, in custom VLSI design, many circuits are entered at the transistor-level to meet high performance goals.
To run formal equivalence checking on custom circuits, an important phase is Transistor-Level Abstraction. Transistor-level abstraction is defined as the process of understanding and translating a transistor netlist to a high-level representation (suitable for simulation by tools such as Verilog®). Common uses for transistor-level abstraction are switch-level simulation, equivalence checking, and ATPG.
An important requirement for abstraction is the ability to understand and “abstract” dynamic CMOS circuits. In order to achieve this, current tools use the Pre-charge Recognition methodology. This is usually done via clock propagation to identify pre-charge nodes. The current tools either abstract the pre-charge logic as part of the design, or eliminate it to match the RTL. Following that step, an equivalence check can be performed on either an RTL with no pre-charge information, or an RTL with detailed pre-charge information.